COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BASL30\M1BASI30\M2NGR40\.
C00006 ENDMK
C⊗;
\\M0BASL30;\M1BASI30;\M2NGR40;\.
\F2\CSTANFORD ARTIFICIAL INTELLIGENCE LABORATORY
\CDEPARTMENT OF COMPUTER SCIENCE
\CSTANFORD UNIVERSITY
\CSTANFORD, CALIFORNIA 94305
\F0





						

							14 October 1974
Professor Dana Scott
Mathematical Institute
24-29 St. Giles
Oxford OX1 3LB
England

Dear Dana:

\J	John Gill gave me your \F1Data Types as Lattices\F0 and thank you
very much.  I am still pursuing my idea of trying to get a system that
will allow the continuous functions to be axiomatized in first order logic
so that we can combine reasoning about other entities with reasoning about
computable functions.  To this end, about two years ago, I introduced the
idea of extensional forms: an e.f. has free variables in it, but two of them
are equal if they give the same values for all values of the free variables.
The λ becomes just another function that combines a variable and a form to
get another form having one less variable.  The idea seems to work out, but
I haven't pushed it quite far enough to really see.

	Your latest seems promising from my point of view, because it gets
all entities down into a fixed domain, e.g. Pw, and this should make set-theoretic
axiomatization easier.  It occurred to me that for practical purposes it might
be even better to use Ps, where s is the set of LISP S-expressions.  Then the
pairing functions, etc. that you use will be \F1conveniently\F0 computable.

	Enclosed is a printout of a set of axioms for extensional forms, but
I am not sure they are comprehensible without more talk.\.

                                                	Best Regards,


	 					        John McCarthy
							Director, Artificial Intelligence Laboratory
							Professor of Computer Science

JMC;paw
scott.le1[let,jmc]:SU-AI